Switch-level analyses on conventional MOS (metal-oxide-semiconductor) often partition an electronic design into a netlist including multiple channel-connected components, construct a reduced order binary decision diagram (ROBDD or simply BDD), and traverse the ROBDD to obtain DC (direct current) or steady-state vectors based on the switch-graph theory. The transistor paths (e.g., a path from an output node to a voltage source Vdd or the ground GND) are then examined to determine the states of the nodes by providing these DC vectors to a simulator to determine switch vectors to sensitize or verify whether the electronic design switches as indicated by these switch vectors.
The size of channel-connected components in modern electronic designs in the past year or two has grown exponentially to have a channel-connected component having more than one hundred (100) MOS transistors or structures. The resulting ROBDDs often include hundreds of thousands of nodes. Sensitizing transistor paths in such an electronic design thus has taken a prohibitively expensive amount of time, especially during the simulation of the DC vectors to obtain the switch vectors.
To further exacerbate the prohibitively long runtime during the simulation stage, such switch-level simulations often assume that a MOS transistor is unidirectional with respect to its gate. That is, these simulations often assume that the voltage at a gate node of a MOS transistor causes some voltage change at the source or drain node, yet the voltages at the source and drain nodes are assumed to have no effect on the voltage of the gate node.
In satisfiability problems, an electronic circuit is often modeled with CNF (conjunctive normal form) formulae. Conventional approaches model an electronic design with CNF at the gate level. Unfortunately, the characteristics (e.g., the bi-directional characteristic) of MOS transistors cannot be successfully modeled and solved at the gate level.
Therefore, there exists a need for a method and a system for implementing an electronic design with transistor-level satisfiability models without having the aforementioned issues, disadvantages, or problems. The advantages of the various embodiments described herein are numerous. Most notably, the methods and systems described herein implement an electronic design with conjunctive normal forms at the transistor level and determine the switch vectors without pre-computing the DC vectors, constructing and traversing a binary decision diagram, or determining switch vectors by performing simulations with the DC vectors.